The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

lte(Cons(x', xs'), Cons(x, xs)) → lte(xs', xs)
lte(Cons(x, xs), Nil) → False
even(Cons(x, Nil)) → False
even(Cons(x', Cons(x, xs))) → even(xs)
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
lte(Nil, y) → True
even(Nil) → True
goal(x, y) → and(lte(x, y), even(x))

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True

Rewrite Strategy: INNERMOST

(1) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
Cons/0

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

lte(Cons(xs'), Cons(xs)) → lte(xs', xs)
lte(Cons(xs), Nil) → False
even(Cons(Nil)) → False
even(Cons(Cons(xs))) → even(xs)
notEmpty(Cons(xs)) → True
notEmpty(Nil) → False
lte(Nil, y) → True
even(Nil) → True
goal(x, y) → and(lte(x, y), even(x))

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True

Rewrite Strategy: INNERMOST

(3) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
lte(Cons(xs'), Cons(xs)) →⁺ lte(xs', xs)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [xs' / Cons(xs'), xs / Cons(xs)].
The result substitution is [ ].

(4) BOUNDS(n^1, INF)